<!doctype html>
<html lang="en">
  <head>
    <!-- Required meta tags -->
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">

    <!-- Bootstrap CSS -->
	<!--<link rel="stylesheet" href="css/bootstrap.min.css" >-->
	<link rel="stylesheet" href="https://leanprover-community.github.io//css/lean.css" >
	<link rel="stylesheet"
          href="https://fonts.googleapis.com/css?family=Merriweather:700">
    

	<script>
                function buildShortcutsForStructures(names) { 
                        const o = {}
                        names.forEach(name => o[name] = `\\mathbb\{${name}\}`)
                        return o
                }
		MathJax = {
			  tex: {
                                  macros: {
                                          ...buildShortcutsForStructures(["R", "Q", "Z", "N", "C"]),
                                  },
				      inlineMath: [['$', '$'], ['\\(', '\\)']]
				    },
		};
	</script>
	<script type="text/javascript" id="MathJax-script" async
		  src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js">
	</script>

	<title>Maths in Lean : category theory</title>
  </head>
  <body>
  <div id="wrapper">
  <nav class="navbar navbar-expand-lg navbar-light bg-gradient-light">
    <div class="d-flex flex-grow-1">
		<a class="navbar-brand" href="https://leanprover-community.github.io/index.html">Lean Community
    </a>
    </div>

    <button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation">
      <span class="navbar-toggler-icon"></span>
    </button>
    <div class="collapse navbar-collapse flex-grow-1 text-right" id="navbarSupportedContent">
      <ul class="navbar-nav ml-auto">
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Try it!
          </a>
		  <div class="dropdown-menu " aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/lean-web-editor">Lean online</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/get_started.html">Install</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Learn
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/learn.html">Resources</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.github.io/theorem_proving_in_lean/">Theorem proving in Lean</a>
			
			
			
			<a class="dropdown-item" href="http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/">The natural number game</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib-overview.html">Library overview</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib_docs">API documentation</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Community
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html">Meet us</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.zulipchat.com/">Zulip chat</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html#maintainers">Maintainers</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/contribute/index.html">How to contribute</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/papers.html">Papers</a>
			
			
          </div>
        </li>
		
      </ul>
    </div>
  </nav>
  <div class="container-sm mt-4">
	  
<h1 id="maths-in-lean--category-theory" class="markdown-heading">Maths in Lean : category theory <a class="hover-link" href="#maths-in-lean--category-theory">#</a></h1>
<p>The <code>category</code> typeclass is defined in <a href="https://leanprover-community.github.io/mathlib_docs/category_theory/category/default.html">category_theory/default.lean</a>.
It depends on the type of the objects, so for example we might write <code>category (Type u)</code> if we're talking about a category whose objects are types (in universe <code>u</code>).</p>
<p>Functors (which are a structure, not a typeclass) are defined in <a href="https://leanprover-community.github.io/mathlib_docs/category_theory/functor.html">category_theory/functor.lean</a>,
along with identity functors and functor composition.</p>
<p>Natural transformations, and their compositions, are defined in <a href="https://leanprover-community.github.io/mathlib_docs/category_theory/natural_transformation.html">category_theory/natural_transformation.lean</a>.</p>
<p>The category of functors and natural transformations between fixed categories <code>C</code> and <code>D</code>
is defined in <a href="https://leanprover-community.github.io/mathlib_docs/category_theory/functor_category.html">category_theory/functor_category.lean</a>.</p>
<p>Cartesian products of categories, functors, and natural transformations appear in
<a href="https://leanprover-community.github.io/mathlib_docs/category_theory/products/basic.html">category_theory/products/basic.lean</a>. (Product in the sense of limits will appear elsewhere soon!)</p>
<p>The category of types, and the hom pairing functor, are defined in <a href="https://leanprover-community.github.io/mathlib_docs/category_theory/types.html">category_theory/types.lean</a>.</p>
<h2 id="notation" class="markdown-heading">Notation <a class="hover-link" href="#notation">#</a></h2>
<h3 id="categories" class="markdown-heading">Categories <a class="hover-link" href="#categories">#</a></h3>
<p>We use the <code>⟶</code> (<code>\hom</code>) arrow to denote sets of morphisms, as in <code>X ⟶ Y</code>.
This leaves the actual category implicit; it is inferred from the type of <code>X</code> and <code>Y</code> by typeclass inference.</p>
<p>We use <code>𝟙</code> (<code>\b1</code>) to denote identity morphisms, as in <code>𝟙 X</code>.</p>
<p>We use <code>≫</code> (<code>\gg</code>) to denote composition of morphisms, as in <code>f ≫ g</code>, which means &quot;<code>f</code> followed by <code>g</code>&quot;.
You may prefer write composition in the usual convention, using <code>⊚</code> (<code>\oo</code> or <code>\circledcirc</code>), as in <code>f ⊚ g</code> which means &quot;<code>g</code> followed by <code>f</code>&quot;. To do so you'll need to add this notation locally, via</p>
<pre><code>local notation f ` ⊚ `:80 g:80 := category.comp g f
</code></pre>
<h3 id="isomorphisms" class="markdown-heading">Isomorphisms <a class="hover-link" href="#isomorphisms">#</a></h3>
<p>We use <code>≅</code> for isomorphisms.</p>
<h3 id="functors" class="markdown-heading">Functors <a class="hover-link" href="#functors">#</a></h3>
<p>We use <code>⥤</code> (<code>\func</code>) to denote functors, as in <code>C ⥤ D</code> for the type of functors from <code>C</code> to <code>D</code>.
(Unfortunately <code>⇒</code> is reserved in <code>logic.relator</code>: https://github.com/leanprover-community/mathlib/blob/master/src/logic/relator.lean, so we can't use that here.)</p>
<p>We use <code>F.obj X</code> to denote the action of a functor on an object.
We use <code>F.map f</code> to denote the action of a functor on a morphism`.</p>
<p>Functor composition can be written as <code>F ⋙ G</code>.</p>
<h3 id="natural-transformations" class="markdown-heading">Natural transformations <a class="hover-link" href="#natural-transformations">#</a></h3>
<p>We use <code>τ.app X</code> for the components of a natural transformation.</p>
<p>Otherwise, we mostly use the notation for morphisms in any category:</p>
<p>We use <code>F ⟶ G</code> (<code>\hom</code> or <code>--&gt;</code>) to denote the type of natural transformations, between functors
<code>F</code> and <code>G</code>.
We use <code>F ≅ G</code> (<code>\iso</code>) to denote the type of natural isomorphisms.</p>
<p>For vertical composition of natural transformations we just use <code>≫</code>. For horizontal composition,
use <code>hcomp</code>.</p>

  </div>
</div>

  <nav class="footer navbar navbar-expand-lg navbar-light bg-light justify-content-end">
  <ul class="nav">
    <li class="nav-item">
      <a class="nav-link active" href="https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/theories/category_theory.md">Suggest edits to this page on GitHub</a>
    </li>
  </ul>
</nav>

    <script src="https://code.jquery.com/jquery-3.4.1.slim.min.js" integrity="sha384-J6qa4849blE2+poT4WnyKhv5vZF5SrPo0iEjwBvKU7imGFAV0wwj1yYfoRSJoZ+n" crossorigin="anonymous"></script>
    <script src="https://leanprover-community.github.io//js/bootstrap.min.js"></script>
    
  </body>
</html>